ePMC

Benchmark
Model:philosophers-mdp v.1 (MDP)
Parameter(s)N = 80
Property:eat (prob-reach)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ../epmc-standard.jar check --model-input-files philosophers-mdp.80.jani --model-input-type jani --property-input-names eat --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6
Execution
Walltime:0.948444128036499s
Return code:1
Log
assertions-disabled
model-checking
analysing-property eat
start-building-explorer
STDERR
Exception in thread "main" java.lang.NullPointerException
	at epmc.jani.extensions.functions.EvaluatorExplicitCall.findFunction(EvaluatorExplicitCall.java:208)
	at epmc.jani.extensions.functions.EvaluatorExplicitCall.<init>(EvaluatorExplicitCall.java:169)
	at epmc.jani.extensions.functions.EvaluatorExplicitCall$Builder.build(EvaluatorExplicitCall.java:108)
	at epmc.expression.standard.evaluatorexplicit.UtilEvaluatorExplicit.newEvaluator(UtilEvaluatorExplicit.java:169)
	at epmc.expression.standard.evaluatorexplicit.EvaluatorExplicitOperatorShortcutAnd.<init>(EvaluatorExplicitOperatorShortcutAnd.java:128)
	at epmc.expression.standard.evaluatorexplicit.EvaluatorExplicitOperatorShortcutAnd$Builder.build(EvaluatorExplicitOperatorShortcutAnd.java:95)
	at epmc.expression.standard.evaluatorexplicit.UtilEvaluatorExplicit.newEvaluator(UtilEvaluatorExplicit.java:169)
	at epmc.expression.standard.evaluatorexplicit.UtilEvaluatorExplicit.newEvaluatorBoolean(UtilEvaluatorExplicit.java:97)
	at epmc.jani.explorer.EdgeEvaluator.<init>(EdgeEvaluator.java:190)
	at epmc.jani.explorer.EdgeEvaluator$Builder.build(EdgeEvaluator.java:156)
	at epmc.jani.explorer.ExplorerComponentAutomaton.buildEdgeEvaluators(ExplorerComponentAutomaton.java:351)
	at epmc.jani.explorer.ExplorerComponentAutomaton.buildAfterVariables(ExplorerComponentAutomaton.java:236)
	at epmc.jani.explorer.ExplorerComponentSynchronisationVectors.buildAfterVariables(ExplorerComponentSynchronisationVectors.java:222)
	at epmc.jani.explorer.ExplorerJANI.prepareSystem(ExplorerJANI.java:276)
	at epmc.jani.explorer.ExplorerJANI.<init>(ExplorerJANI.java:206)
	at epmc.jani.explorer.ExplorerJANI.<init>(ExplorerJANI.java:174)
	at epmc.jani.explorer.ExplorerJANI$Builder.build(ExplorerJANI.java:127)
	at epmc.jani.explorer.ExplorerJANI$Builder.build(ExplorerJANI.java:82)
	at epmc.modelchecker.UtilModelChecker.buildLowLevel(UtilModelChecker.java:150)
	at epmc.jani.explorer.LowLevelExplicitBuilder.build(LowLevelExplicitBuilder.java:63)
	at epmc.modelchecker.UtilModelChecker.buildLowLevel(UtilModelChecker.java:150)
	at epmc.modelchecker.UtilModelChecker.buildLowLevel(UtilModelChecker.java:169)
	at epmc.modelchecker.ModelChecker.prepareLowLevel(ModelChecker.java:222)
	at epmc.modelchecker.ModelChecker.checkProperty(ModelChecker.java:247)
	at epmc.modelchecker.ModelChecker.check(ModelChecker.java:192)
	at epmc.command.CommandTaskCheck.executeInServer(CommandTaskCheck.java:64)
	at epmc.jani.interaction.Analyse.execute(Analyse.java:111)
	at epmc.jani.interaction.commandline.StartInConsoleJaniInteractionNoJani.execute(StartInConsoleJaniInteractionNoJani.java:91)
	at epmc.jani.interaction.commandline.StartInConsoleJaniInteractionNoJani.process(StartInConsoleJaniInteractionNoJani.java:68)
	at epmc.main.EPMC.main(EPMC.java:52)